package arlab.formulae
//import arlab.formulae._
import arlab.formulae.transformations._


/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.120
 * Time: 12:42
 * To change this template use File | Settings | File Templates.
 */

// Allquantor besteht aus Variable und ihrem Scope
object ClauseSet{

  def create (fm: Formula): List[List[Formula]] = Transformations.cnf(Transformations.simplify(Transformations.matrix(Transformations.skolemize(fm)))) match {

    //case And(a,b) =>
    case Or(a,b) => List(getClause(fm, List()))
    case And(a,b) => create(a) ++ create(b)
    case other => List(List(other))
    //case other => other
    
    
  }

  def getClause (fm: Formula, ls:List[Formula]) : List[Formula] = fm match {
    case Or(Or(a,b),c) => getClause (Or(a,b), ls :+ c)
    case Or(a,Or(b,c)) => getClause (Or(b,c), ls :+ a)
    case Or(a,b) => (ls :+ a) :+ b
  }
}
